\begin{tabbing}
causal{-}bijection(${\it es}$;$a$.$f$($a$);$e$.$P$($e$);${\it e'}$.$Q$(${\it e'}$);$R$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=Bij(\{$e$:es{-}E(${\it es}$)$\mid$ $P$($e$)\} ;\{${\it e'}$:es{-}E(${\it es}$)$\mid$ $Q$(${\it e'}$)\} ;$\lambda$$a$.$f$($a$))\+
\\[0ex]\& ($\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $P$($e$)\} . es{-}causle(${\it es}$;$e$;$f$($e$)) \& $R$(es{-}val(${\it es}$; $e$),es{-}val(${\it es}$; $f$($e$))))
\-
\end{tabbing}